es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p, q, p',
q':({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
(a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  {p(a,b)  p'(a,b)})
 (a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  {q(a,b)  q'(a,b)})
 {[e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  [e1;e2]~([a,b].p'(a,b))*[a,b].q'(a,b)} 

latex

Definitions

x:A. B(x), {i..j}, t  T, E, Id, P  Q, False, A, P & Q, AB, i  j < k, , x(s1,s2), pred(e), (x  l), P  Q, loc(e), P  Q, b, x. t(x), (e <loc e'), P  Q, ES, 1of(t), e  e' , True, T, A & B, x:A. B(x), Prop, [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), [e, e'], x,y. t(x;y), {T}, Trans x,y:T. E(x;y), SQType(T), S  T, S  T

Lemmas

es-le-self, es-pred-le, es-le-pred, es-increasing-sequence2, member-es-interval, es-le-trans, l member wf, es-interval wf, es-pstar-q wf, es-le wf, es-locl wf, exists functionality wrt iff, and functionality wrt iff, int seg wf, es-pred wf, squash wf, true wf, event system wf, int seg properties, nat plus properties, es-le-loc, es-loc-pred, or functionality wrt iff, all functionality wrt iff, es-locl-iff, es-E wf, Id wf, es-loc wf, le wf, l member subtype